/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.gameSolver.NuGat;

import com.sun.jna.Library;
import com.sun.jna.Pointer;

//Libraries to export structs (not used anymore)
//import com.ochafik.lang.jnaerator.runtime.Structure;
//import com.ochafik.lang.jnaerator.runtime.Union;

//wrapper for CUDD from PRISM (not used anymore)
//import jdd.JDDNode;

/**
 * 
 * WARNING : never use a function that has a boolean or a long return value or
 * paramater!
 * 
 * 
 * This class is an interface for NuGat/NuSmv. For declare a new wrapper to a C
 * function, just add : {public|private} type name(paramaters).
 *
 * The following convention is used :
 *  -put on comment on the top of declaration, the C file where function is defined.
 *  -to return a pointer use Pointer and put on comment //return C structure
 *  -to name parameter the syntax is Pointer CStructure_name.
 *
 * You can also generate this file, or a part via jnaerator.
 *
 *
 * @author simon
 */


public interface NuGatInterface extends Library {

    //*********************************** CUDD *******************************//
    //cuddUtils.c
    public Pointer 
        Cudd_SubsetWithMaskVars(
          Pointer DdManager,
          Pointer DdNode_f, //function from which to pick a cube
          Pointer[] DdNode_vars, //array of variables
          int  nvars, //size of vars
          Pointer[] DdNode_maskVars, //array of variables
          int  mvars //size of maskVars
        );//return ddNode* (bdd_ptr)  
    
    public Pointer 
            Cudd_bddExistAbstract(
              Pointer DdManager, 
              Pointer DdNode_f, 
              Pointer DdNode_cube 
            );//return DdNode * (bdd_ptr)
    
    public Pointer 
            Cudd_CubeArrayToBdd(
              Pointer DdManager, 
              int[] array 
            ); //return DdNode * (bdd_ptr)

    
    //*********************************** NUSMV ******************************//

    public void util_getopt_reset();

    //NuSmv cmd/cmd.h
    public Pointer CmdOpenFile(String filename);

    //NuSmv parser/parser.h
    public int Parser_ReadSMVFromFile(String fileName);
    public void Parser_Init();

    //NuSmv opt/opt.h
    public void init_options_cmd();

    //NuSmv sm/sm.h
    public int Sm_NusmvrcSource();

    //NuSmv enc/enc.c
    public Pointer Enc_get_bdd_encoding();//return bddEnc_ptr
    public Pointer Enc_get_bool_encoding();//return BoolEnc_ptr
    
    //NuSmv enc/utils/utils.c
    public Pointer enc_utils_parse_ordering_file(String order_filename, 
                              Pointer bool_enc); //return OrdGroups_ptr 
    
    //NuSmv enc/bdd/BddEnc.c
    public Pointer BddEnc_get_dd_manager(Pointer BddEnc_ptr);//return DdManager*
    public Pointer BddEnc_get_layer_vars_cube(Pointer BddEnc_ptr ,
                                         Pointer SymbLayer_ptr_layer,
                                         int SymbFilterType_vt);
    public Pointer BddEnc_state_var_to_next_state_var(Pointer BddEnc_ptr,
            Pointer bdd_ptr);//return bdd_ptr
    public Pointer BddEnc_expr_to_bdd(Pointer BddEnc_ptr, Pointer Expr_ptr,
                           Pointer node_ptr_context);//return bdd_ptr
    
    public Pointer BddEnc_create(Pointer symb_table,
                         Pointer bool_enc, Pointer DdManager,
                         Pointer ord_groups); //return BddEnc_ptr
    public void BddEnc_force_order (Pointer BddEnc_ptr, Pointer OrdGroups_ptr_new_po_grps);
    public Pointer BddEnc_get_state_vars_cube (Pointer BddEnc_ptr);//return bdd_ptr
    public Pointer BddEnc_get_next_state_vars_cube (Pointer BddEnc_ptr);//return bdd_ptr

    //NuSmv enc/bdd/BddEncPrintWff.c

    public void BddEnc_print_bdd_wff(Pointer BddEnc_ptr,
                          Pointer bdd_ptr,         /* the input bdd */
                          Pointer NodeList_ptr_vars,   /* variables */
                          boolean do_sharing,  /* requires dag sharing */
                          boolean do_indent,   /* requires indentation */
                          int start_at_column, /* align to column (indent only) */
                          Pointer file            /* the stream to write to */
                          );
    public Pointer BddEnc_bdd_to_expr(Pointer BddEnc_ptr, Pointer bdd_ptr);//return node_ptr
    public Pointer BddEnc_bdd_to_wff(
                           Pointer BddEnc, 
                           Pointer bdd,        /* the input bdd */
                           Pointer NodeList_ptr_vars   /* variables */
                           );//return node_ptr


    
    //NuSmv enc/base/baseEnc.c
    public void BaseEnc_commit_layer(Pointer BaseEnc_ptr,String layer_name);
    public void BaseEnc_remove_layer(Pointer BaseEnc_ptr, String layer_name);
    public void base_enc_remove_layer(Pointer BaseEnc_ptr, String layer_name);


    //NuSmv opt/OptsHandler.c
    public Pointer OptsHandler_get_instance();
    
    //NuSmv opt/optCmd.c
    public void set_pgm_path(Pointer opt, String str);
    public void unset_batch(Pointer opt);
    public void set_input_file(Pointer opt, String fileNameModel);
    public void set_input_order_file(Pointer opt,
            String fileNameOrderModel);
    public Pointer get_partition_method(Pointer opt);
    public String get_input_order_file(Pointer opt);
    public int get_verbose_level(Pointer OptsHandler_ptr );

    //NuSmv compile/compileCmd.c
    public int CommandWriteOrder(int argc, String[] argv);
    public int CommandShowVars(int argc, String[] argv);
    
    //NuSmv compile/compileStruct.c
    public Pointer Compile_get_global_fsm_builder();

    //NuSmv compile/compile.h
    public Pointer Compile_get_global_symb_table();
    public Pointer sym_intern(String s); //return node_ptr

    //NuSmv compile/symb_table/symbTable.c
    public Pointer SymbTable_get_layer(Pointer SymbTable_ptr, String layer_name);
    public Pointer SymbTable_get_vars (Pointer SymbTable_ptr);//return NodeList_ptr
    public Pointer SymbTable_create_layer(Pointer SymbTable_ptr,
                                     String layer_name,
                                     int LayerInsertPolicy_ins_policy); //return SymbLayer_ptr
    public Pointer SymbTable_get_layers_sf_i_vars(Pointer SymbTable_ptr,
                               Pointer layer_names);//return NodeLis_ptr
    
    public void SymbTable_remove_layer(Pointer SymbTable_ptr, Pointer SymbLayer_ptr);
    
    //NuSmv compile/symb_table/symbLayer.c
    public void SymbLayer_declare_state_var(Pointer SymbLayer_ptr, Pointer node_ptr_var_name, 
                                 Pointer SymbType_ptr_type);
    public String SymbLayer_get_name(Pointer SymbLayer_ptr);
    public int Chameleon_SymbLayer_can_declare_var (Pointer SymbLayer_ptr, 
                                Pointer node_ptr_name);


    //NuSmv compile/FlatHierarchy.c
    public Pointer FlatHierarchy_create(Pointer SymbTable_ptr);// return FlatHierarchy_ptr
    public Pointer FlatHierarchy_get_trans(Pointer FlatHierarchy_ptr);//return node_ptr
    public void FlatHierarchy_set_trans(Pointer FlatHierarchy_ptr ,Pointer node_ptr);

    
    //NuSmv compile/compileFlatten.c
    public Pointer CompileFlatten_expand_range(int a, int b); //return node_ptr
    
    
    //NuSmv compile/SymbType.c
    public Pointer SymbType_create(int SymbTypeTag_tag, Pointer node_ptr_body); //return SymbType_ptr

    //NuSmv prop/prop.c
    public String Prop_get_type_as_string(Pointer Prop_ptr);
    public int Prop_get_type(Pointer Prop_ptr);//Prop_Type
    public Pointer Prop_get_expr_core(Pointer Prop_ptr);//return Expr_ptr
    public String Prop_get_text (Pointer Prop_ptr);
    public int Prop_get_status(Pointer Prop_ptr);
    public void Prop_set_bdd_fsm (Pointer Prop_ptr,Pointer BddFsm_ptr);
    public Pointer Prop_create_partial(Pointer Expr_ptr, int Prop_Type);//return  Prop_ptr
    public void Prop_set_scalar_sexp_fsm(Pointer Prop_ptr , Pointer SexpFsm_ptr);

    //NuSmv prop/propPkg.c
    public Pointer PropPkg_get_prop_database();//return propDb_ptr
    
    //NuSmv prop/propDb.c    
    public void PropDb_master_set_bdd_fsm(Pointer PropDb_ptr_self, Pointer BddFsm_ptr_fsm);

    //NuSmv fsm/bdd/bddFsm.c
    public Pointer BddFsm_get_trans(Pointer bddFsm_ptr);//return BddTrans_ptr
    public Pointer  BddFsm_create (Pointer BddEnc_ptr_encoding,Pointer BddStates_init, 
                    Pointer BddInvarStates_invar_states, Pointer BddInvarInputs_invar_inputs, 
                    Pointer BddTrans_ptr_trans, 
                    Pointer JusticeList_ptr_justice,Pointer  CompassionList_ptr_compassion);//return BddFsm_ptr
    public Pointer  BddFsm_get_justice(Pointer bddFsm_ptr);//return JusticeList_ptr
    public Pointer  BddFsm_get_compassion(Pointer bddFsm_ptr);//return CompassionList_ptr
    public Pointer  BddFsm_get_state_constraints(Pointer bddFsm_ptr);//return BddInvarStates
    public Pointer  BddFsm_get_input_constraints(Pointer bddFsm_ptr);//return BddInvarInputs
    public void BddFsm_apply_synchronous_product(Pointer BddFsm_ptr_self, Pointer BddFsm_ptr_other);
    public Pointer BddFsm_get_bdd_encoding(Pointer BddFsm_ptr); //return BddEnc_ptr
    public Pointer BddFsm_get_init(Pointer BddFsm_ptr); //return BddStates 
    public void BddFsm_print_info (Pointer BddFsm_ptr, Pointer file);
    public Pointer BddFsm_get_monolithic_trans_bdd(Pointer BddFsm_ptr);//return bdd_ptr 
    public Pointer BddFsm_copy(Pointer BddFsm_ptr);//return BddFsm_ptr
    
    //NuSmv fsm/bdd/fairnessList.c
    public Pointer CompassionList_create (Pointer dd_manager);//return compassion_ptr
    public Pointer JusticeList_create(Pointer dd_manager);//return justice_ptr
    
    //NuSmv ltl/ltl.c
    public void Chameleon_Ltl_CheckLtlSpec(Pointer Prop_ptr);
    public Pointer Ltl_StructCheckLtlSpec_create();//return Ltl_StructCheckLtlSpec_ptr
    public void Ltl_StructCheckLtlSpec_set_prop(Pointer Ltl_StructCheckLtlSpec_ptr,
                                     Pointer Prop_ptr);
    public void Ltl_StructCheckLtlSpec_set_oreg2smv(Pointer Ltl_StructCheckLtlSpec_ptr ,
                                        Pointer Ltl_StructCheckLtlSpec_oreg2smv );

    //NuSmv utils/NodeList.c
    public void NodeList_print_nodes(Pointer NodeList_ptr, Pointer out);
    public Pointer NodeList_to_node_ptr(Pointer NodeList_ptr);//return node_ptr
    public Pointer NodeList_get_first_iter(Pointer NodeList_ptr); //return ListIter_ptr
    public Pointer ListIter_get_next(Pointer ListIter_ptr ); //return ListIter_ptr
    public Pointer NodeList_get_elem_at(Pointer NodeList_ptr, Pointer ListIter_ptr);//return  node_ptr
    public void NodeList_concat(Pointer NodeList_self, Pointer NodeList_src);
    


    //NuSmv utils/uString.c
    public Pointer find_string(String text);//return string_ptr
    public String get_text (Pointer string_ptr);

    //NuSmv node/node.h
    public int print_node (Pointer file ,Pointer node_ptr);
    public int print_sexp (Pointer file ,Pointer node_ptr);
    public String sprint_node (Pointer node_ptr);

    //NuSmv node/node.c
    public Pointer cdr(Pointer node_ptr_x); //return node_ptr
    public Pointer car(Pointer node_ptr_x); //return node_ptr
    public Pointer cons(Pointer node_ptr_x, Pointer node_ptr_y);//return node_ptr
    public Pointer new_node(int type, Pointer node_ptr_left, Pointer node_ptr_right);//return node_ptr
    public Pointer find_node(int type, Pointer node_ptr_left, Pointer node_ptr_right);//return node_ptr
    public Pointer reverse(Pointer node_ptr_x);//return node_ptr
    public void free_node(Pointer node_ptr);
    public int llength(Pointer node_ptr_r);
    public int Chameleon_node_get_type(Pointer node_ptr);
    
    //NuSmv trans/BddTrans.h
    public Pointer  BddTrans_create(Pointer dd_manager,
                             Pointer clusters_bdd,
                             Pointer state_vars_cube,
                             Pointer input_vars_cube,
                             Pointer next_state_vars_cube,
                             Pointer trans_type,
                             Pointer ClusterOptions_ptr);//return BddTrans_ptr
    public void BddTrans_apply_synchronous_product(Pointer BddTrans_ptr_self,
                                        Pointer BddTrans_ptr_other,
                                        Pointer bdd_ptr_state_vars_cube,
                                        Pointer bdd_ptr_input_vars_cube,
                                        Pointer bdd_ptr_next_state_vars_cube);


    //NuSmv fsm/Sexp/SexpFsm.c
    public Pointer  SexpFsm_get_vars_list(Pointer SexpFsm_ptr);//return NodeList_ptr
    public Pointer SexpFsm_get_var_trans(Pointer SexpFsm_ptr,Pointer node_ptr_var_name);//Expr_ptr

    //NuSmv fsm/sexp/eprc.c
    public Pointer Expr_and_nil(Pointer Expr_ptr_a, Pointer Expr_ptr_b);//return Expr_ptr

    //NuSmv fsm/FsmBuilder.c
    public Pointer fsm_builder_order_vars_list(Pointer FsmBuilder_ptr ,
                                         Pointer BddEnc_ptr ,
                                         Pointer NodeList_ptr_vars);//return Set_t
    public Pointer fsm_builder_clusterize_expr(Pointer FsmBuilder_ptr,
                                                   Pointer BddEnc_ptr,
                                                   Pointer Expr_ptr);//return  ClusterList_ptr

    //NuSmv set/setSet.c
    public Pointer Set_GetFirstIter(Pointer Set_t); //return Set_Iterator_t
    public Pointer Set_GetNextIter(Pointer Set_Iterator_t);//return Set_Iterator_t
    public Pointer Set_GetMember(Pointer Set_t, Pointer Set_Iterator_t);//Set_Element_t
    public void Set_ReleaseSet(Pointer Set_t );

    //NuSmv trans/bdd/ClusterOptions.c
    public Pointer ClusterOptions_create(Pointer OptsHandler_ptr_options);//return ClusterOptions_ptr
    public void ClusterOptions_destroy(Pointer ClusterOptions_ptr);

    //NuSmv trans/bdd/ClusterList.c
    public void ClusterList_destroy(Pointer ClusterList_ptr);

    //NuSmv dd/dd.c
    public Pointer bdd_one(Pointer DdManager);//return bdd_ptr
    public Pointer bdd_zero(Pointer DdManager);//return bdd_ptr
    public Pointer bdd_and(Pointer DdManager, Pointer bdd_ptr_a,Pointer  bdd_ptr_b);//return bdd_ptr
    public Pointer bdd_or(Pointer DdManager, Pointer bdd_ptr_a,Pointer  bdd_ptr_b);//return bdd_ptr
    public Pointer bdd_dup(Pointer dd_node);//return bdd_ptr
    public void bdd_free(Pointer DdManager,Pointer bdd_ptr_dd_node);
    public void bdd_deref(Pointer dd_node);
    public Pointer init_dd_package();//return DdManager *
    public Pointer bdd_not(Pointer DdManager, Pointer bdd_ptr_fn);//return bdd_ptr
    public int bdd_is_zero(Pointer DdManager, Pointer bdd_ptr_f);
    public int bdd_is_one(Pointer DdManager, Pointer bdd_ptr_f);
    public int bdd_isnot_zero(Pointer DdManager ,Pointer bdd_ptr_f);
    public int bdd_size(Pointer DdManager ,Pointer bdd_ptr_fn);
    public int dd_get_size(Pointer DdManager );
    public Pointer bdd_new_var_with_index(Pointer DdManager, int index);//return bdd_ptr
    public void bdd_ref(Pointer bdd_ptr_dd_node);
    

    //******************************** NUGAT *********************************//

     //NuGat addons/game/gameCmd.c
    public int game_invoke_game_command(int argc, String[] argv, int type);
    public int CommandGameBuildFlatModel (int argc, String[] argv);
    public int CommandGameBuildBooleanModel (int argc, String[] argv);
    public int CommandGameBuildModel(int argc, String[] argv);
    public void Game_quit_cmd();
    public int CommandCheckLtlGameSpecSF07(int argc, String[] argv);
    public int CommandGameWriteModelFlat(int argc, String[] argv);


    //NuGat addons/game/gameBuildModel.c
    public void Game_CommandBuildFlatModel();
    public void Game_CommandBuildBooleanModel();
    public void Game_CommandBuildBddModel();
    public Pointer Game_CreateGameBddFsm(Pointer fsm_builder,
                                     Pointer enc,
                                     Pointer sexp_fsm,
                                     Pointer layer_1,
                                     Pointer layer_2,
                                     Pointer trans_type);

    //NuGat addons/game/gameFlatten.
    public int Game_CommandFlattenHierarchy();

    //NuGat smgame/smgameInt.h
    public void Smgame_Init();

    //NUGat addons/game/gameVarEncoding.c
    public int Game_CommandEncodeVariables(String input_order_file_name);

    //NuGat addons/game/PropDbGame.c
    public Pointer PropDbGame_master_get_game_scalar_sexp_fsm(Pointer PropDbGame_ptr); //return GameSexpFsm_ptr
    public void PropDbGame_master_set_game_bdd_fsm(Pointer PropDbGame_ptr, Pointer fsm);
    public Pointer PropDbGame_master_get_game_bdd_fsm(Pointer PropDbGame_ptr);

    //NuGat addons/game/PropGame.c
    public Pointer PropGame_get_game_bdd_fsm(Pointer PropGame_ptr);//return GameBddFsm_ptr
    public Pointer PropGame_get_player(Pointer PropGame_ptr);//string_ptr
    public Pointer PropGame_create_partial(Pointer Expr_ptr, int PropGame_Type);//return  PropGame_ptr
    public void PropGame_set_game_bdd_fsm (Pointer PropGame_ptr_self,
                                            Pointer GameBddFsm_ptr_fsm);

    //NuGat addons/game/fsm/gameBddFsm.c
    public Pointer GameBddFsm_get_player_1(Pointer gameBddFsm);//return bddFsm_ptr
    public Pointer GameBddFsm_get_player_2(Pointer gameBddFsm);//return bddFsm_ptr
    public void GameBddFsm_print_info (Pointer GameBddFsm_ptr, Pointer file);
    public Pointer GameBddFsm_get_init_1(Pointer GameBddFsm_ptr);//return BddStates
    public Pointer GameBddFsm_get_init_2(Pointer GameBddFsm_ptr);//return BddStates
    public Pointer GameBddFsm_get_invars_1(Pointer GameBddFsm_ptr);//return BddInvarStates
    public Pointer GameBddFsm_get_invars_2(Pointer GameBddFsm_ptr);//return BddInvarStates
    public boolean GameBddFsm_can_player_satisfy(Pointer GameBddFsm_ptr,
                                             Pointer BddStates_constr_1,
                                             Pointer BddStates_constr_2,
                                             Pointer BddStates_goalStates,
                                             Pointer GamePlayer_player,
                                             char quantifiers);
    public Pointer GameBddFsm_get_strong_backward_image(Pointer GameBddFsm_ptr,
                                               Pointer BddStates_goal,
                                               Pointer GamePlayer_player);//return  BddStates
    
    public Pointer GameBddFsm_get_move(Pointer GameBddFsm_ptr,
                                Pointer BddStates_toState,
                                Pointer GamePlayer_player); //return BddStates
    
    public Pointer GameBddFsm_without_successor_states(Pointer GameBddFsm_ptr,
                                           Pointer GamePlayer ); //return BddStates
    
    public Pointer GameBddFsm_player_satisfies_from(Pointer GameBddFsm_ptr,
                                                  Pointer BddStates_constr_1,
                                                  Pointer BddStates_constr_2,
                                                  Pointer BddStates_goalStates,
                                                  Pointer GamePlayer_player,
                                                  char quantifiers); //return BddStates 
    public Pointer GameBddFsm_copy (Pointer GameBddFsm_ptr );//return GameBddFsm_ptr 
    
    public Pointer GameBddFsm_create(Pointer enc,
                                 Pointer player_1,
                                 Pointer stateVarCube_1,
                                 Pointer stateFrozenVarCube_1,
                                 Pointer player_2,
                                 Pointer stateVarCube_2,
                                 Pointer stateFrozenVarCube_2);
    public Pointer GameBddFsm_get_state_var_cube_1(Pointer GameBddFsm_ptr);//return bdd_ptr
    public Pointer GameBddFsm_get_state_var_cube_2(Pointer GameBddFsm_ptr);//return bdd_ptr
    public Pointer GameBddFsm_get_state_frozen_var_cube_1(Pointer GameBddFsm_ptr);//return bdd_ptr
    public Pointer GameBddFsm_get_state_frozen_var_cube_2(Pointer GameBddFsm_ptr);//return bdd_ptr
    

    //NuGat addons/game/fsm/gameSexpFsm.c
    public Pointer GameSexpFsm_get_vars_list_1(Pointer gameSexpFsm); //return NodeList pointer
    public Pointer GameSexpFsm_get_vars_list_2(Pointer gameSexpFsm); //return NodeList pointer
    public Pointer GameSexpFsm_get_player_1 (Pointer GameSexpFsm_ptr);//return SexpFsm_ptr
    public Pointer GameSexpFsm_get_player_2 (Pointer GameSexpFsm_ptr);//return SexpFsm_ptr

    //NuGat addons/game/gameReqToGame.c
    public Pointer game_and_exp( Pointer node_ptr_exp1, Pointer node_ptr_exp2);//return node_ptr


    //NuGat addons/game/gameGeneral.c
    public void Game_BeforeCheckingSpec(Pointer PropGame_ptr_prop);

    //NuGat addons/game/gamePlayer.c
    public Pointer Game_StrToPlayer(Pointer string_ptr);//return GamePlayer
    public Pointer Game_PlayerToStr(Pointer GamePlayer_player); //return String_ptr

    //NuGat addons/game/gameOpt.c
    public char opt_game_game_initial_condition(Pointer OptsHandler_ptr_opt);
    public int get_game_sf07_strategy_printing_mode(Pointer OptsHandler_ptr_opt);

    //NuGat addons/game/GameCheckReachAvoidSpec.c
    public int isTargetReached(Pointer fsm, Pointer bdd_ptr_init_1, Pointer bdd_ptr_init_2,
	Pointer bdd_ptr_allReachStates,Pointer GamePlayer_player, char quantifiers);
    

    //NuGat addons/game/GameStrategy.c
    public Pointer GameStrategy_create(Pointer BddEnc_ptr_bdd_enc,
                                     Pointer GamePlayer_player,
                                     int reverseInitialQuantifiers,
                                     Pointer bdd_ptr_init_goal,
                                     Pointer bdd_ptr_init_opponent_deadlock,
                                     Pointer bdd_ptr_init_moves,
                                     Pointer bdd_ptr_goal,
                                     Pointer bdd_ptr_opponent_deadlock,
                                     Pointer bdd_ptr_moves);//return GameStrategy_ptr
    public Pointer GameStrategy_construct(Pointer GameBddFsm_ptr,
                                        Pointer GamePlayer,
                                        int reverseInitialQuantifiers,
                                        Pointer bdd_ptr_goal,
                                        Pointer bdd_ptr_winningStates,
                                        Pointer bdd_ptr_trans);//return GameStrategy_ptr 
    public Pointer GameStrategy_get_bdd_enc(Pointer GameStrategy_ptr); //return BddEnc_ptr
    public Pointer GameStrategy_get_player(Pointer  GameStrategy_ptr); //return  GamePlayer
    public Pointer GameStrategy_get_init_goal(Pointer GameStrategy_ptr); //return bdd_ptr
    public Pointer GameStrategy_get_init_opponent_deadlock(Pointer GameStrategy_ptr);//return bdd_ptr
    public Pointer GameStrategy_get_init_moves(Pointer GameStrategy_ptr);//return bdd_ptr
    public Pointer GameStrategy_get_goal(Pointer GameStrategy_ptr);//return bdd_ptr
    public Pointer GameStrategy_get_opponent_deadlock(Pointer GameStrategy_ptr);//return bdd_ptr
    public Pointer GameStrategy_get_moves(Pointer GameStrategy_ptr);//return bdd_ptr
    public int GameStrategy_get_isSuccess(Pointer GameStrategy_ptr);
    public void GameStrategy_set_init_goal(Pointer GameStrategy_ptr,Pointer bdd_ptr_init_goal);
    public void GameStrategy_set_init_opponent_deadlock(Pointer GameStrategy_ptr,Pointer bdd_ptr_init_opponent_deadlock);
    public void GameStrategy_set_init_moves(Pointer GameStrategy_ptr, Pointer bdd_ptr_init_moves);
    public void GameStrategy_set_goal(Pointer GameStrategy_ptr, Pointer bdd_ptr_goal);
    public void GameStrategy_set_opponent_deadlock(Pointer GameStrategy_ptr,Pointer bdd_ptr_opponent_deadlock);
    public void GameStrategy_set_moves(Pointer GameStrategy_ptr, Pointer bdd_ptr_moves);
    public void GameStrategy_destroy (Pointer GameStrategy_ptr);
    
    //NuGat addons/game/GameGeneral.c
    public void Chameleon_Game_AfterCheckingSpec(Pointer PropGame_ptr_prop,
                            int Game_RealizabilityStatus_status,
                            Pointer GameStrategy_ptr_strategy,
                            Pointer node_ptr_varList1,
                            Pointer node_ptr_varList2,
                            int strategy_printout,
                            int printout_as_dag,
                            int indented_printout,
                            String file);
     public Pointer Chameleon_createParams(int strategy_printout,
                                            int printout_as_dag,
                                            int indented_printout,
                                            String file);//return gameParams_ptr
    
    
    //NuGat addons/game/gamePkg.c
    public void Game_Quit();
    
    //NuGat addons/game/gameCheckGen... .c
    public Pointer Chameleon_Game_CheckGenReactivitySpec(Pointer PropGame_ptr_prop,
            Pointer node_ptr_var,int constructStrategy);//return GameStrategy_ptr
    public Pointer Chameleon_Game_CheckBuchiGameSpec(Pointer PropGame_ptr_prop, 
            Pointer node_ptr_var, int constructStrategy);//return GameStrategy_ptr
    
    public int Chameleon_game_compute_gen_reactivity(Pointer node_ptr_specExp,
                                          int player,
                                          Pointer GameBddFsm_ptr_fsm);
    
    public int Chameleon_game_compute_buchi_game(Pointer PropGame_ptr_prop);
    
    //NuGaT addons/game/gameCheckLtlGameSF07.c
    public Pointer
        Game_SF07_StructCheckLTLGameSF07_create(Pointer PropGame_ptr_prop,
                                                Pointer gameParams_ptr_params,
                                                int kmin,
                                                int kmax,
                                                int Game_Who_w); //return Game_SF07_StructCheckLTLGameSF07_ptr
    
    public Pointer Chameleon_Game_SF07_StructCheckLTLGameSF07_get_player(Pointer Game_SF07_StructCheckLTLGameSF07_ptr);
    public Pointer Chameleon_Game_SF07_StructCheckLTLGameSF07_get_prop
            (Pointer Game_SF07_StructCheckLTLGameSF07_ptr);//return PropGame_ptr
    public Pointer Chameleon_Game_SF07_StructCheckLTLGameSF07_get_strategy(Pointer Game_SF07_StructCheckLTLGameSF07_ptr);
    public Pointer Chameleon_Game_SF07_StructCheckLTLGameSF07_get_BddEnc(Pointer Game_SF07_StructCheckLTLGameSF07_ptr );
    public void Chameleon_Game_SF07_StructCheckLTLGameSF07_set_params (Pointer Game_SF07_StructCheckLTLGameSF07_ptr,
            Pointer gameParams_ptr);
    public void Game_SF07_StructCheckLTLGameSF07_run_iteration
                (Pointer Game_SF07_StructCheckLTLGameSF07_ptr,
                 int curr_k,
                 int curr_player);
    public void Chameleon_Game_SF07_StructCheckLTLGameSF07_print_strategy_monitor_sexp
            (Pointer Game_SF07_StructCheckLTLGameSF07_ptr,int strategy_printout,
                                                        int printout_as_dag,
							int indented_printout,
							String file );
    public void Chameleon_Game_SF07_StructCheckLTLGameSF07_print_strategy_monitor_bdd
            (Pointer Game_SF07_StructCheckLTLGameSF07_ptr,int strategy_printout,
                                                        int printout_as_dag,
							int indented_printout,
							String file );
    public void Game_SF07_StructCheckLTLGameSF07_destroy(Pointer self);
    public Pointer Chameleon_Game_SF07_StructCheckLTLGameSF07_get_layer_of_player_1(Pointer self);//return SymbLayer_ptr
    public Pointer Chameleon_Game_SF07_StructCheckLTLGameSF07_get_layer_of_player_2(Pointer self);//return SymbLayer_ptr
    public Pointer Chameleon_Game_SF07_StructCheckLTLGameSF07_get_curr_player2_monitor_sexp_copy(Pointer self);//return node_ptr
    
    public Pointer Chameleon_get_layers();
    public Pointer Chameleon_get_layers_to_decl(Pointer structLtl);
    

    public String PLAYER_NAME_1 = "PLAYER_1";
    public String PLAYER_NAME_2 = "PLAYER_2";
    public String LAYER_PLAYER_1 = "layer_of_PLAYER_1";
    public String LAYER_PLAYER_2 = "layer_of_PLAYER_2";
    
    //******************************* ENUM **********************************//

    
                   
    public static final int Prop_NoStatus = (int)0;
    public static final int Prop_Unchecked = (int)1;
    public static final int Prop_True = (int)2;
    public static final int Prop_False = (int)3;
    public static final int Prop_Number = (int)4;
    
    public static final int GAME_SF07_STRATEGY_PRINTING_MODE_SEXP = (int)0;
    

    
    /**
        * Do not touch this<br>
	* <i>native declaration : line 2</i>
     */
    public static final int PropGame_PropGame_Type_First = (int)200;
    /**
     * Game specifications: ReachTarget should be the first and<br>
     * GenReactivity should be the last in game specs.<br>
     * Game specifications: ReachTarget should be the first and<br>
     * GenReactivity should be the last in game specs.<br>
     * <i>native declaration : line 6</i>
     */
    public static final int PropGame_ReachTarget = (int)201;
    /// <i>native declaration : line 7</i>
    public static final int PropGame_AvoidTarget = (int)202;
    /// <i>native declaration : line 8</i>
    public static final int PropGame_ReachDeadlock = (int)203;
    /// <i>native declaration : line 9</i>
    public static final int PropGame_AvoidDeadlock = (int)204;
    /// <i>native declaration : line 10</i>
    public static final int PropGame_BuchiGame = (int)205;
    /// <i>native declaration : line 11</i>
    public static final int PropGame_LtlGame = (int)206;
    /// <i>native declaration : line 12</i>
    public static final int PropGame_GenReactivity = (int)207;
    /**
     * ----------------------------------------------------------------------<br>
     * ----------------------------------------------------------------------<br>
     * Do not touch this<br>
     * <i>native declaration : line 14</i>
     */
    public static final int PropGame_PropGame_Type_Last = (int)208;
    public static final int GAME_REALIZABLE = (int)0;
    public static final int GAME_UNREALIZABLE = (int)1;
    public static final int GAME_UNKNOWN = (int)2;
    public static final int SYMB_LAYER_POS_BOTTOM = (int)3;
    public static final int SYMB_TYPE_ENUM = (int)2;
    
    public static final int GAME_INIT_TERM_NONE = (int)1;
    public static final int GAME_INIT_TERM_NORMAL = (int)2;
    public static final int GAME_INIT_TERM_CONJUNCT = (int)3;
    
    public static final int GAME_SPEC_WRAPPER = (int)2011;
    public static final int GAME_EXP_LIST = (int)2012;
    public static final int GAME_TWO_EXP_LISTS = (int)2013;
    
    public static final int PLAYER_1 = (int)0;
    public static final int PLAYER_2 = (int)1;
    
    public static final int Prop_Ltl = (int)103;
    
                /// <i>native declaration : line 2</i>
		public static final int GAME_WHO_INVALID = (int)-1;
		/// <i>native declaration : line 3</i>
		public static final int GAME_WHO_NONE = (int)0;
		/// <i>native declaration : line 4</i>
		public static final int GAME_WHO_BOTH = (int)1;
		/// <i>native declaration : line 5</i>
		public static final int GAME_WHO_PROTAGONIST = (int)2;
		/// <i>native declaration : line 6</i>
		public static final int GAME_WHO_ANTAGONIST = (int)3;
		/// <i>native declaration : line 7</i>
		public static final int GAME_WHO_PLAYER_1 = (int)4;
		/// <i>native declaration : line 8</i>
		public static final int GAME_WHO_PLAYER_2 = (int)5;
		/// <i>native declaration : line 9</i>
		public static final int GAME_WHO_WINNER = (int)6;
		/// <i>native declaration : line 10</i>
		public static final int GAME_WHO_LOSER = (int)7;


	/**
	 * <i>native declaration : line 1</i><br>
	 * enum values
	 */
	
		/// <i>native declaration : line 2</i>
		public static final int NUSMV_CORE_SYMBOL_FIRST = (int)100;
		/**
		 * ----------------------------------------------------------------------<br>
		 * ----------------------------------------------------------------------<br>
		 * <i>native declaration : line 5</i>
		 */
		public static final int NUSMV_STATEMENTS_SYMBOL_FIRST = NUSMV_CORE_SYMBOL_FIRST;
		/**
		 * 101<br>
		 * <i>native declaration : line 7</i>
		 */
		public static final int TRANS = (int)NUSMV_CORE_SYMBOL_FIRST + 1;
		/// <i>native declaration : line 8</i>
		public static final int INIT = (int)NUSMV_CORE_SYMBOL_FIRST + 2;
		/// <i>native declaration : line 9</i>
		public static final int INVAR = (int)NUSMV_CORE_SYMBOL_FIRST + 3;
		/// <i>native declaration : line 10</i>
		public static final int ASSIGN = (int)NUSMV_CORE_SYMBOL_FIRST + 4;
		/// <i>native declaration : line 11</i>
		public static final int FAIRNESS = (int)NUSMV_CORE_SYMBOL_FIRST + 5;
		/// <i>native declaration : line 12</i>
		public static final int JUSTICE = (int)NUSMV_CORE_SYMBOL_FIRST + 6;
		/// <i>native declaration : line 13</i>
		public static final int COMPASSION = (int)NUSMV_CORE_SYMBOL_FIRST + 7;
		/// <i>native declaration : line 14</i>
		public static final int SPEC = (int)NUSMV_CORE_SYMBOL_FIRST + 8;
		/// <i>native declaration : line 15</i>
		public static final int LTLSPEC = (int)NUSMV_CORE_SYMBOL_FIRST + 9;
		/**
		 * 110<br>
		 * <i>native declaration : line 16</i>
		 */
		public static final int PSLSPEC = (int)NUSMV_CORE_SYMBOL_FIRST + 10;
		/// <i>native declaration : line 17</i>
		public static final int INVARSPEC = (int)NUSMV_CORE_SYMBOL_FIRST + 11;
		/// <i>native declaration : line 18</i>
		public static final int COMPUTE = (int)NUSMV_CORE_SYMBOL_FIRST + 12;
		/// <i>native declaration : line 19</i>
		public static final int DEFINE = (int)NUSMV_CORE_SYMBOL_FIRST + 13;
		/// <i>native declaration : line 20</i>
		public static final int ISA = (int)NUSMV_CORE_SYMBOL_FIRST + 14;
		/// <i>native declaration : line 21</i>
		public static final int GOTO = (int)NUSMV_CORE_SYMBOL_FIRST + 15;
		/// <i>native declaration : line 22</i>
		public static final int CONSTRAINT = (int)NUSMV_CORE_SYMBOL_FIRST + 16;
		/// <i>native declaration : line 23</i>
		public static final int MODULE = (int)NUSMV_CORE_SYMBOL_FIRST + 17;
		/// <i>native declaration : line 24</i>
		public static final int PROCESS = (int)NUSMV_CORE_SYMBOL_FIRST + 18;
		/// <i>native declaration : line 25</i>
		public static final int MODTYPE = (int)NUSMV_CORE_SYMBOL_FIRST + 19;
		/**
		 * 120<br>
		 * <i>native declaration : line 26</i>
		 */
		public static final int LAMBDA = (int)NUSMV_CORE_SYMBOL_FIRST + 20;
		/// <i>native declaration : line 27</i>
		public static final int CONSTANTS = (int)NUSMV_CORE_SYMBOL_FIRST + 21;
		/// <i>native declaration : line 29</i>
		public static final int PRED = (int)NUSMV_CORE_SYMBOL_FIRST + 22;
		/// <i>native declaration : line 30</i>
		public static final int ATTIME = (int)NUSMV_CORE_SYMBOL_FIRST + 23;
		/// <i>native declaration : line 31</i>
		public static final int PREDS_LIST = (int)NUSMV_CORE_SYMBOL_FIRST + 24;
		/// <i>native declaration : line 32</i>
		public static final int MIRROR = (int)NUSMV_CORE_SYMBOL_FIRST + 25;
		/// <i>native declaration : line 34</i>
		public static final int NUSMV_STATEMENTS_SYMBOL_LAST = (int)NUSMV_CORE_SYMBOL_FIRST + 26;
		/**
		 * ----------------------------------------------------------------------<br>
		 * ----------------------------------------------------------------------<br>
		 * <i>native declaration : line 39</i>
		 */
		public static final int NUSMV_EXPR_SYMBOL_FIRST = (int)NUSMV_CORE_SYMBOL_FIRST + 27;
		/// <i>native declaration : line 41</i>
		public static final int FAILURE = (int)NUSMV_CORE_SYMBOL_FIRST + 28;
		/// <i>native declaration : line 42</i>
		public static final int CONTEXT = (int)NUSMV_CORE_SYMBOL_FIRST + 29;
		/// <i>native declaration : line 43</i>
		public static final int EU = (int)NUSMV_CORE_SYMBOL_FIRST + 30;
		/// <i>native declaration : line 44</i>
		public static final int AU = (int)NUSMV_CORE_SYMBOL_FIRST + 31;
		/// <i>native declaration : line 45</i>
		public static final int EBU = (int)NUSMV_CORE_SYMBOL_FIRST + 32;
		/// <i>native declaration : line 46</i>
		public static final int ABU = (int)NUSMV_CORE_SYMBOL_FIRST + 33;
		/// <i>native declaration : line 47</i>
		public static final int MINU = (int)NUSMV_CORE_SYMBOL_FIRST + 34;
		/// <i>native declaration : line 48</i>
		public static final int MAXU = (int)NUSMV_CORE_SYMBOL_FIRST + 35;
		/// <i>native declaration : line 49</i>
		public static final int VAR = (int)NUSMV_CORE_SYMBOL_FIRST + 36;
		/// <i>native declaration : line 50</i>
		public static final int FROZENVAR = (int)NUSMV_CORE_SYMBOL_FIRST + 37;
		/// <i>native declaration : line 51</i>
		public static final int IVAR = (int)NUSMV_CORE_SYMBOL_FIRST + 38;
		/// <i>native declaration : line 52</i>
		public static final int BOOLEAN = (int)NUSMV_CORE_SYMBOL_FIRST + 39;
		/**
		 * 140<br>
		 * <i>native declaration : line 53</i>
		 */
		public static final int ARRAY = (int)NUSMV_CORE_SYMBOL_FIRST + 40;
		/// <i>native declaration : line 54</i>
		public static final int OF = (int)NUSMV_CORE_SYMBOL_FIRST + 41;
		/// <i>native declaration : line 55</i>
		public static final int SCALAR = (int)NUSMV_CORE_SYMBOL_FIRST + 42;
		/// <i>native declaration : line 56</i>
		public static final int CONS = (int)NUSMV_CORE_SYMBOL_FIRST + 43;
		/// <i>native declaration : line 57</i>
		public static final int BDD = (int)NUSMV_CORE_SYMBOL_FIRST + 44;
		/// <i>native declaration : line 58</i>
		public static final int SEMI = (int)NUSMV_CORE_SYMBOL_FIRST + 45;
		/// <i>native declaration : line 59</i>
		public static final int LP = (int)NUSMV_CORE_SYMBOL_FIRST + 46;
		/// <i>native declaration : line 60</i>
		public static final int RP = (int)NUSMV_CORE_SYMBOL_FIRST + 47;
		/// <i>native declaration : line 61</i>
		public static final int LB = (int)NUSMV_CORE_SYMBOL_FIRST + 48;
		/// <i>native declaration : line 62</i>
		public static final int RB = (int)NUSMV_CORE_SYMBOL_FIRST + 49;
		/// <i>native declaration : line 63</i>
		public static final int LCB = (int)NUSMV_CORE_SYMBOL_FIRST + 50;
		/// <i>native declaration : line 64</i>
		public static final int RCB = (int)NUSMV_CORE_SYMBOL_FIRST + 51;
		/// <i>native declaration : line 65</i>
		public static final int EQDEF = (int)NUSMV_CORE_SYMBOL_FIRST + 52;
		/// <i>native declaration : line 66</i>
		public static final int TWODOTS = (int)NUSMV_CORE_SYMBOL_FIRST + 53;
		/// <i>native declaration : line 67</i>
		public static final int FALSEEXP = (int)NUSMV_CORE_SYMBOL_FIRST + 54;
		/// <i>native declaration : line 68</i>
		public static final int TRUEEXP = (int)NUSMV_CORE_SYMBOL_FIRST + 55;
		/// <i>native declaration : line 69</i>
		public static final int SELF = (int)NUSMV_CORE_SYMBOL_FIRST + 56;
		/// <i>native declaration : line 70</i>
		public static final int CASE = (int)NUSMV_CORE_SYMBOL_FIRST + 57;
		/// <i>native declaration : line 71</i>
		public static final int ESAC = (int)NUSMV_CORE_SYMBOL_FIRST + 58;
		/// <i>native declaration : line 72</i>
		public static final int COLON = (int)NUSMV_CORE_SYMBOL_FIRST + 59;
		/**
		 * 160<br>
		 * <i>native declaration : line 73</i>
		 */
		public static final int IFTHENELSE = (int)NUSMV_CORE_SYMBOL_FIRST + 60;
		/// <i>native declaration : line 74</i>
		public static final int INCONTEXT = (int)NUSMV_CORE_SYMBOL_FIRST + 61;
		/// <i>native declaration : line 75</i>
		public static final int SIMPWFF = (int)NUSMV_CORE_SYMBOL_FIRST + 62;
		/// <i>native declaration : line 76</i>
		public static final int NEXTWFF = (int)NUSMV_CORE_SYMBOL_FIRST + 63;
		/// <i>native declaration : line 77</i>
		public static final int LTLWFF = (int)NUSMV_CORE_SYMBOL_FIRST + 64;
		/// <i>native declaration : line 78</i>
		public static final int CTLWFF = (int)NUSMV_CORE_SYMBOL_FIRST + 65;
		/// <i>native declaration : line 79</i>
		public static final int COMPWFF = (int)NUSMV_CORE_SYMBOL_FIRST + 66;
		/// <i>native declaration : line 80</i>
		public static final int ATOM = (int)NUSMV_CORE_SYMBOL_FIRST + 67;
		/// <i>native declaration : line 81</i>
		public static final int NUMBER = (int)NUSMV_CORE_SYMBOL_FIRST + 68;
		/// <i>native declaration : line 82</i>
		public static final int COMMA = (int)NUSMV_CORE_SYMBOL_FIRST + 69;
		/// <i>native declaration : line 83</i>
		public static final int IMPLIES = (int)NUSMV_CORE_SYMBOL_FIRST + 70;
		/// <i>native declaration : line 84</i>
		public static final int IFF = (int)NUSMV_CORE_SYMBOL_FIRST + 71;
		/// <i>native declaration : line 85</i>
		public static final int OR = (int)NUSMV_CORE_SYMBOL_FIRST + 72;
		/// <i>native declaration : line 86</i>
		public static final int XOR = (int)NUSMV_CORE_SYMBOL_FIRST + 73;
		/// <i>native declaration : line 87</i>
		public static final int XNOR = (int)NUSMV_CORE_SYMBOL_FIRST + 74;
		/// <i>native declaration : line 88</i>
		public static final int AND = (int)NUSMV_CORE_SYMBOL_FIRST + 75;
		/// <i>native declaration : line 89</i>
		public static final int NOT = (int)NUSMV_CORE_SYMBOL_FIRST + 76;
		/// <i>native declaration : line 90</i>
		public static final int EX = (int)NUSMV_CORE_SYMBOL_FIRST + 77;
		/// <i>native declaration : line 91</i>
		public static final int AX = (int)NUSMV_CORE_SYMBOL_FIRST + 78;
		/// <i>native declaration : line 92</i>
		public static final int EF = (int)NUSMV_CORE_SYMBOL_FIRST + 79;
		/**
		 * 180<br>
		 * <i>native declaration : line 93</i>
		 */
		public static final int AF = (int)NUSMV_CORE_SYMBOL_FIRST + 80;
		/// <i>native declaration : line 94</i>
		public static final int EG = (int)NUSMV_CORE_SYMBOL_FIRST + 81;
		/// <i>native declaration : line 95</i>
		public static final int AG = (int)NUSMV_CORE_SYMBOL_FIRST + 82;
		/// <i>native declaration : line 96</i>
		public static final int EE = (int)NUSMV_CORE_SYMBOL_FIRST + 83;
		/// <i>native declaration : line 97</i>
		public static final int AA = (int)NUSMV_CORE_SYMBOL_FIRST + 84;
		/// <i>native declaration : line 98</i>
		public static final int SINCE = (int)NUSMV_CORE_SYMBOL_FIRST + 85;
		/// <i>native declaration : line 99</i>
		public static final int UNTIL = (int)NUSMV_CORE_SYMBOL_FIRST + 86;
		/// <i>native declaration : line 100</i>
		public static final int TRIGGERED = (int)NUSMV_CORE_SYMBOL_FIRST + 87;
		/// <i>native declaration : line 101</i>
		public static final int RELEASES = (int)NUSMV_CORE_SYMBOL_FIRST + 88;
		/// <i>native declaration : line 102</i>
		public static final int EBF = (int)NUSMV_CORE_SYMBOL_FIRST + 89;
		/// <i>native declaration : line 103</i>
		public static final int EBG = (int)NUSMV_CORE_SYMBOL_FIRST + 90;
		/// <i>native declaration : line 104</i>
		public static final int ABF = (int)NUSMV_CORE_SYMBOL_FIRST + 91;
		/// <i>native declaration : line 105</i>
		public static final int ABG = (int)NUSMV_CORE_SYMBOL_FIRST + 92;
		/// <i>native declaration : line 106</i>
		public static final int BUNTIL = (int)NUSMV_CORE_SYMBOL_FIRST + 93;
		/// <i>native declaration : line 107</i>
		public static final int MMIN = (int)NUSMV_CORE_SYMBOL_FIRST + 94;
		/// <i>native declaration : line 108</i>
		public static final int MMAX = (int)NUSMV_CORE_SYMBOL_FIRST + 95;
		/// <i>native declaration : line 109</i>
		public static final int OP_NEXT = (int)NUSMV_CORE_SYMBOL_FIRST + 96;
		/// <i>native declaration : line 110</i>
		public static final int OP_GLOBAL = (int)NUSMV_CORE_SYMBOL_FIRST + 97;
		/// <i>native declaration : line 111</i>
		public static final int OP_FUTURE = (int)NUSMV_CORE_SYMBOL_FIRST + 98;
		/// <i>native declaration : line 112</i>
		public static final int OP_PREC = (int)NUSMV_CORE_SYMBOL_FIRST + 99;
		/**
		 * 200<br>
		 * <i>native declaration : line 113</i>
		 */
		public static final int OP_NOTPRECNOT = (int)NUSMV_CORE_SYMBOL_FIRST + 100;
		/// <i>native declaration : line 114</i>
		public static final int OP_HISTORICAL = (int)NUSMV_CORE_SYMBOL_FIRST + 101;
		/// <i>native declaration : line 115</i>
		public static final int OP_ONCE = (int)NUSMV_CORE_SYMBOL_FIRST + 102;
		/// <i>native declaration : line 116</i>
		public static final int EQUAL = (int)NUSMV_CORE_SYMBOL_FIRST + 103;
		/// <i>native declaration : line 117</i>
		public static final int NOTEQUAL = (int)NUSMV_CORE_SYMBOL_FIRST + 104;
		/// <i>native declaration : line 118</i>
		public static final int LT = (int)NUSMV_CORE_SYMBOL_FIRST + 105;
		/// <i>native declaration : line 119</i>
		public static final int GT = (int)NUSMV_CORE_SYMBOL_FIRST + 106;
		/// <i>native declaration : line 120</i>
		public static final int LE = (int)NUSMV_CORE_SYMBOL_FIRST + 107;
		/// <i>native declaration : line 121</i>
		public static final int GE = (int)NUSMV_CORE_SYMBOL_FIRST + 108;
		/// <i>native declaration : line 122</i>
		public static final int UNION = (int)NUSMV_CORE_SYMBOL_FIRST + 109;
		/// <i>native declaration : line 123</i>
		public static final int SETIN = (int)NUSMV_CORE_SYMBOL_FIRST + 110;
		/// <i>native declaration : line 124</i>
		public static final int MOD = (int)NUSMV_CORE_SYMBOL_FIRST + 111;
		/// <i>native declaration : line 125</i>
		public static final int PLUS = (int)NUSMV_CORE_SYMBOL_FIRST + 112;
		/// <i>native declaration : line 126</i>
		public static final int MINUS = (int)NUSMV_CORE_SYMBOL_FIRST + 113;
		/// <i>native declaration : line 127</i>
		public static final int TIMES = (int)NUSMV_CORE_SYMBOL_FIRST + 114;
		/// <i>native declaration : line 128</i>
		public static final int DIVIDE = (int)NUSMV_CORE_SYMBOL_FIRST + 115;
		/// <i>native declaration : line 129</i>
		public static final int UMINUS = (int)NUSMV_CORE_SYMBOL_FIRST + 116;
		/// <i>native declaration : line 130</i>
		public static final int NEXT = (int)NUSMV_CORE_SYMBOL_FIRST + 117;
		/// <i>native declaration : line 131</i>
		public static final int SMALLINIT = (int)NUSMV_CORE_SYMBOL_FIRST + 118;
		/// <i>native declaration : line 132</i>
		public static final int DOT = (int)NUSMV_CORE_SYMBOL_FIRST + 119;
		/**
		 * 220<br>
		 * <i>native declaration : line 133</i>
		 */
		public static final int BIT = (int)NUSMV_CORE_SYMBOL_FIRST + 120;
		/// <i>native declaration : line 134</i>
		public static final int RANGE = (int)NUSMV_CORE_SYMBOL_FIRST + 121;
		/**
		 * identifies expressions and types<br>
		 * <i>native declaration : line 135</i>
		 */
		public static final int UNSIGNED_WORD = (int)NUSMV_CORE_SYMBOL_FIRST + 122;
		/**
		 * identifies types<br>
		 * <i>native declaration : line 136</i>
		 */
		public static final int SIGNED_WORD = (int)NUSMV_CORE_SYMBOL_FIRST + 123;
		/// <i>native declaration : line 137</i>
		public static final int INTEGER = (int)NUSMV_CORE_SYMBOL_FIRST + 124;
		/// <i>native declaration : line 138</i>
		public static final int REAL = (int)NUSMV_CORE_SYMBOL_FIRST + 125;
		/**
		 * identifies constants<br>
		 * <i>native declaration : line 139</i>
		 */
		public static final int NUMBER_UNSIGNED_WORD = (int)NUSMV_CORE_SYMBOL_FIRST + 126;
		/**
		 * identifies constants<br>
		 * <i>native declaration : line 140</i>
		 */
		public static final int NUMBER_SIGNED_WORD = (int)NUSMV_CORE_SYMBOL_FIRST + 127;
		/// <i>native declaration : line 141</i>
		public static final int NUMBER_FRAC = (int)NUSMV_CORE_SYMBOL_FIRST + 128;
		/// <i>native declaration : line 142</i>
		public static final int NUMBER_REAL = (int)NUSMV_CORE_SYMBOL_FIRST + 129;
		/**
		 * 230<br>
		 * <i>native declaration : line 143</i>
		 */
		public static final int NUMBER_EXP = (int)NUSMV_CORE_SYMBOL_FIRST + 130;
		/// <i>native declaration : line 144</i>
		public static final int LSHIFT = (int)NUSMV_CORE_SYMBOL_FIRST + 131;
		/// <i>native declaration : line 145</i>
		public static final int RSHIFT = (int)NUSMV_CORE_SYMBOL_FIRST + 132;
		/// <i>native declaration : line 146</i>
		public static final int LROTATE = (int)NUSMV_CORE_SYMBOL_FIRST + 133;
		/// <i>native declaration : line 147</i>
		public static final int RROTATE = (int)NUSMV_CORE_SYMBOL_FIRST + 134;
		/// <i>native declaration : line 148</i>
		public static final int BIT_SELECTION = (int)NUSMV_CORE_SYMBOL_FIRST + 135;
		/// <i>native declaration : line 149</i>
		public static final int CONCATENATION = (int)NUSMV_CORE_SYMBOL_FIRST + 136;
		/// <i>native declaration : line 150</i>
		public static final int CAST_BOOL = (int)NUSMV_CORE_SYMBOL_FIRST + 137;
		/// <i>native declaration : line 151</i>
		public static final int CAST_WORD1 = (int)NUSMV_CORE_SYMBOL_FIRST + 138;
		/// <i>native declaration : line 152</i>
		public static final int CAST_SIGNED = (int)NUSMV_CORE_SYMBOL_FIRST + 139;
		/// <i>native declaration : line 153</i>
		public static final int CAST_UNSIGNED = (int)NUSMV_CORE_SYMBOL_FIRST + 140;
		/**
		 * extend the width of a word (signed or unsigned)<br>
		 * <i>native declaration : line 154</i>
		 */
		public static final int EXTEND = (int)NUSMV_CORE_SYMBOL_FIRST + 141;
		/**
		 * 240<br>
		 * 240<br>
		 * <i>native declaration : line 155</i>
		 */
		public static final int WORDARRAY = (int)NUSMV_CORE_SYMBOL_FIRST + 142;
		/// <i>native declaration : line 156</i>
		public static final int WAREAD = (int)NUSMV_CORE_SYMBOL_FIRST + 143;
		/// <i>native declaration : line 157</i>
		public static final int WAWRITE = (int)NUSMV_CORE_SYMBOL_FIRST + 144;
		/**
		 * these are removed by the flattener, so after flattening<br>
		 * <i>native declaration : line 158</i>
		 */
		public static final int UWCONST = (int)NUSMV_CORE_SYMBOL_FIRST + 145;
		/**
		 * they do not exist anywhere<br>
		 * <i>native declaration : line 159</i>
		 */
		public static final int SWCONST = (int)NUSMV_CORE_SYMBOL_FIRST + 146;
		/// <i>native declaration : line 160</i>
		public static final int WRESIZE = (int)NUSMV_CORE_SYMBOL_FIRST + 147;
		/// <i>native declaration : line 161</i>
		public static final int WSIZEOF = (int)NUSMV_CORE_SYMBOL_FIRST + 148;
		/// <i>native declaration : line 162</i>
		public static final int WTOINT = (int)NUSMV_CORE_SYMBOL_FIRST + 149;
		/**
		 * Used for comparing properties ids<br>
		 * <i>native declaration : line 164</i>
		 */
		public static final int COMPID = (int)NUSMV_CORE_SYMBOL_FIRST + 150;
		/**
		 * Used to represent generic array type<br>
		 * <i>native declaration : line 166</i>
		 */
		public static final int ARRAY_TYPE = (int)NUSMV_CORE_SYMBOL_FIRST + 151;
		/**
		 * Define obtained via Matrix-Define<br>
		 * <i>native declaration : line 167</i>
		 */
		public static final int ARRAY_DEF = (int)NUSMV_CORE_SYMBOL_FIRST + 152;
		/// <i>native declaration : line 169</i>
		public static final int NFUNCTION = (int)NUSMV_CORE_SYMBOL_FIRST + 153;
		/// <i>native declaration : line 171</i>
		public static final int NUSMV_EXPR_SYMBOL_LAST = (int)NUSMV_CORE_SYMBOL_FIRST + 154;
		/// <i>native declaration : line 174</i>
		public static final int NUSMV_CORE_SYMBOL_LAST = (int)NUSMV_CORE_SYMBOL_FIRST + 155;


  


	


}
